Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		sum(cons(s(n),x),cons(m,y))	→ sum(cons(n,x),cons(s(m),y))
2:		sum(cons(0,x),y)	→ sum(x,y)
3:		sum(nil,y)	→ y
4:		weight(cons(n,cons(m,x)))	→ weight(sum(cons(n,cons(m,x)),cons(0,x)))
5:		weight(cons(n,nil))	→ n

There are 4 dependency pairs:


6:		SUM(cons(s(n),x),cons(m,y))	→ SUM(cons(n,x),cons(s(m),y))
7:		SUM(cons(0,x),y)	→ SUM(x,y)
8:		WEIGHT(cons(n,cons(m,x)))	→ WEIGHT(sum(cons(n,cons(m,x)),cons(0,x)))
9:		WEIGHT(cons(n,cons(m,x)))	→ SUM(cons(n,cons(m,x)),cons(0,x))

The approximated dependency graph contains 2 SCCs: {6,7} and {8}.

Consider the SCC {6,7}. There are no usable rules. By taking the AF π with π(SUM) = 1 and π(cons) = [2] together with the lexicographic path order with empty precedence, rule 6 is weakly decreasing and rule 7 is strictly decreasing. There is one new SCC.
- Consider the SCC {6}. By taking the AF π with π(cons) = π(SUM) = 1 together with the lexicographic path order with empty precedence, rule 6 is strictly decreasing.

Consider the SCC {8}. The usable rules are {1-3}. By taking the AF π with π(WEIGHT) = 1, π(sum) = 2 and π(cons) = [2] together with the lexicographic path order with empty precedence, the rules in {1-3} are weakly decreasing and rule 8 is strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.03 seconds) --- May 4, 2006